Nuprl Lemma : R-Feasible-Rplus
0,22
postcript
pdf
A
,
B
:Top. R-Feasible(
A
B
) ~ (R-Feasible(
A
) & R-Feasible(
B
) &
A
||
B
)
latex
Definitions
x
:
A
.
B
(
x
)
,
R-Feasible(
R
)
,
t
T
Lemmas
top
wf
origin
A, B:Top. R-Feasible(A 
B) ~ (R-Feasible(A) & R-Feasible(B) & A || B) A, B:Top. R-Feasible(A B) ~ (R-Feasible(A) & R-Feasible(B) & A || B) x:A. B(x)
T